MAYBE 1.974
↳ HASKELL
↳ BR
((enumFrom :: Int -> [Int]) :: Int -> [Int]) |
import qualified Prelude |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((enumFrom :: Int -> [Int]) :: Int -> [Int]) |
import qualified Prelude |
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
((enumFrom :: Int -> [Int]) :: Int -> [Int]) |
import qualified Prelude |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ Narrow
(enumFrom :: Int -> [Int]) |
import qualified Prelude |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ QDP
↳ RuleRemovalProof
↳ Narrow
new_numericEnumFrom(vx3) → new_numericEnumFrom(new_ps(vx3))
new_primPlusNat(Zero) → Succ(Zero)
new_ps(Neg(Succ(Zero))) → Pos(Zero)
new_ps(Neg(Zero)) → Pos(Succ(Zero))
new_ps(Neg(Succ(Succ(vx3000)))) → Neg(Succ(vx3000))
new_primPlusNat0(Succ(vx3000)) → Succ(vx3000)
new_primPlusNat(Succ(vx300)) → Succ(Succ(new_primPlusNat0(vx300)))
new_ps(Pos(vx30)) → Pos(new_primPlusNat(vx30))
new_primPlusNat0(Zero) → Zero
new_ps(Neg(Succ(Zero)))
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)
new_ps(Neg(Succ(Succ(x0))))
new_primPlusNat0(Zero)
new_ps(Pos(x0))
new_ps(Neg(Zero))
new_primPlusNat0(Succ(x0))
new_ps(Neg(Succ(Zero))) → Pos(Zero)
new_ps(Neg(Zero)) → Pos(Succ(Zero))
POL(Neg(x1)) = 1 + x1
POL(Pos(x1)) = 2·x1
POL(Succ(x1)) = x1
POL(Zero) = 0
POL(new_numericEnumFrom(x1)) = 2·x1
POL(new_primPlusNat(x1)) = x1
POL(new_primPlusNat0(x1)) = x1
POL(new_ps(x1)) = x1
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ NonTerminationProof
↳ Narrow
new_numericEnumFrom(vx3) → new_numericEnumFrom(new_ps(vx3))
new_primPlusNat(Zero) → Succ(Zero)
new_ps(Neg(Succ(Succ(vx3000)))) → Neg(Succ(vx3000))
new_primPlusNat0(Succ(vx3000)) → Succ(vx3000)
new_primPlusNat(Succ(vx300)) → Succ(Succ(new_primPlusNat0(vx300)))
new_ps(Pos(vx30)) → Pos(new_primPlusNat(vx30))
new_primPlusNat0(Zero) → Zero
new_ps(Neg(Succ(Zero)))
new_primPlusNat(Succ(x0))
new_primPlusNat(Zero)
new_ps(Neg(Succ(Succ(x0))))
new_primPlusNat0(Zero)
new_ps(Pos(x0))
new_ps(Neg(Zero))
new_primPlusNat0(Succ(x0))
new_numericEnumFrom(vx3) → new_numericEnumFrom(new_ps(vx3))
new_primPlusNat(Zero) → Succ(Zero)
new_ps(Neg(Succ(Succ(vx3000)))) → Neg(Succ(vx3000))
new_primPlusNat0(Succ(vx3000)) → Succ(vx3000)
new_primPlusNat(Succ(vx300)) → Succ(Succ(new_primPlusNat0(vx300)))
new_ps(Pos(vx30)) → Pos(new_primPlusNat(vx30))
new_primPlusNat0(Zero) → Zero